P:prop{i:l}, Q:isect(P; x.prop{i:l}).
decidable(P)  (P  decidable(Q))  decidable((P c Q)) 

latex

Definitions	t  T, P  Q, prop{i:l}, x:A. B(x), decidable(P), A c B, P  Q, guard(T), A, False
Lemmas	decidable wf, not wf